SMT2 solver: implement get-value #3461
Conversation
kroening
commented
Nov 24, 2018
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
kroening
requested review from
chrisr-diffblue,
martin-cs,
peterschrammel,
smowton and
tautschnig
as code owners
kroening
force-pushed
the
smt2_solver_get-value
branch
2 times, most recently
from
d6f97aa to
81690a5
Compare
kroening
force-pushed
the
smt2_solver_get-value
branch
from
81690a5 to
d6f7c5a
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d6f7c5a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92464624
| NOT_SOLVED, | ||
| SAT, | ||
| UNSAT | ||
| } status; |
There was a problem hiding this comment.
Why do we need yet another status enum? We have one for decision procedures, one in prop.h - wouldn't the latter be the right one?
There was a problem hiding this comment.
No; this isn't a result from a solver, but the state of the SMT2-LIB protocol between the solver and the client. The key question is whether (check-sat) has been called or not.
There was a problem hiding this comment.
Maybe such things could be documented in future? The code only did a straightforward translation from enum values of one type to enum values of another type.
